s-insert(x; l)
== rec-case(l) of [] => cons(x; []) | a::as => v.if (x = a)
== rec-case(l) of [] => cons(x; []) | a::as => v.ifthen cons(a; as)
== if x <z a then cons(x; cons(a; as)) else cons(a; v) fi  

latex

Definitions	rec-case(a) of [] => s | x::y => z.t(x;y;z), [], (i = j), if b then t else f fi , i <z j, cons(car; cdr)
FDL editor aliases	s-insert